package fst.calculi.STLC

import fst.parsing._
import fst.binding.Binding

trait Evaluation {
  val syntax: Substitution
  import syntax._
  
  def eval(tm: Term): Term = tm match {
    case App(Abs(_, \\(x, t)), v) if v.isValue => subst(t, x, v)
    case App(v, t) if v.isValue => App(v, eval(t))
    case App(t1, t2) => App(eval(t1), t2)
  }
  
  // transitive closure
  def evalX(tm: Term): Term = tm match {
    case v if v.isValue => v
    case tm => evalX(eval(tm)) // TODO: check this is tail-recursive
  }
}

object EvalTest extends Parsing with Evaluation {
  object syntax extends Substitution
  
  def main(args: Array[String]) = println(for(p <- parse(args(0))) yield evalX(p))
}